home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Languages / Caml Light 0.7 / examples / kb / equation.ml next >
Encoding:
Text File  |  1995-06-19  |  2.3 KB  |  91 lines  |  [TEXT/MPS ]
  1. (****************** Equation manipulations *************)
  2.  
  3. #open "prelude";;
  4. #open "terms";;
  5.  
  6. type rule == int * (int * (term * term));;
  7.  
  8. (* standardizes an equation so its variables are 1,2,... *)
  9.  
  10. let mk_rule m n =
  11.   let all_vars = union (vars m) (vars n) in
  12.   let (k,subst) =
  13.     it_list (fun (i,sigma) v -> (i+1,(v,Var(i))::sigma)) (1,[]) all_vars in
  14.   (k-1, (substitute subst m, substitute subst n))
  15. ;;
  16.  
  17. (* checks that rules are numbered in sequence and returns their number *)
  18. let (check_rules: rule list -> int) =
  19.   it_list (fun n (k,_) -> if k=n+1 then k
  20.                           else failwith "Rule numbers not in sequence") 0
  21. ;;
  22.  
  23. let pretty_rule (k,(_,(m,n)): rule) =
  24.   print_int k; print_string " : ";
  25.   pretty_term m; print_string " = "; pretty_term n;
  26.   print_newline()
  27. ;;
  28.  
  29. let pretty_rules = do_list pretty_rule
  30. ;; 
  31.  
  32. (****************** Rewriting **************************)
  33.  
  34. (* Top-level rewriting. Let eq:l=r be an equation, m be a term such that l<=m.
  35.    With sigma = matching l m, we define the image of m by eq as sigma(r) *)
  36. let reduce l m =
  37.   substitute (matching l m)
  38. ;;
  39.  
  40. (* A more efficient version of can (rewrite1 (l,r)) for r arbitrary *)
  41. let reducible l = redrec
  42.   where rec redrec m =
  43.     try
  44.       matching l m; true
  45.     with Failure _ ->
  46.       match m with Term(_,sons) -> exists redrec sons
  47.                 |         _     -> false
  48. ;;
  49.  
  50. (* mreduce : rules -> term -> term *)
  51. let mreduce rules m =
  52.   let redex (_,(_,(l,r))) = reduce l m r in try_find redex rules
  53. ;;
  54.  
  55. (* One step of rewriting in leftmost-outermost strategy, with multiple rules *)
  56. (* fails if no redex is found *)
  57. (* mrewrite1 : rules -> term -> term *)
  58. let mrewrite1 rules = rewrec
  59.   where rec rewrec m =
  60.     try
  61.       mreduce rules m
  62.     with Failure _ ->
  63.       let rec tryrec = function
  64.           [] -> failwith "mrewrite1"
  65.         | son::rest ->
  66.             try
  67.               rewrec son :: rest
  68.             with Failure _ ->
  69.               son :: tryrec rest in
  70.       match m with
  71.           Term(f, sons) -> Term(f, tryrec sons)
  72.         | _ -> failwith "mrewrite1"
  73. ;;
  74.  
  75. (* Iterating rewrite1. Returns a normal form. May loop forever *)
  76. (* mrewrite_all : rules -> term -> term *)
  77. let mrewrite_all rules m = rew_loop m
  78.   where rec rew_loop m =
  79.     try
  80.       rew_loop(mrewrite1 rules m)
  81.     with Failure _ ->
  82.       m
  83. ;;
  84.  
  85. (*
  86. pretty_term (mrewrite_all Group_rules m where m,_=<<A*(I(B)*B)>>);;
  87. ==> A*U
  88. *)
  89.  
  90.  
  91.